| Definitions |  e@i.P(e), A c B, x:A. B(x), {T}, SQType(T),  e@i. P(e), @i k(v:T) triggers local action a when P (x:A) v, pre-p-realizable, discrete-pre-p-realizable, Top, Normal(T), Rplus-right(x1), Rplus-left(x1), tt, Rplus?(x1), Y, reduce(f;k;as),  (L), recognizer-realizable, es-real-monotonicity, recognizer-p-realizable, es-realizer(p), t.2, True, if b then t else f fi , ff, eq_atom$n(x;y), Atom2Deq, IdDeq, t.1, eqof(d), P & Q, P    Q, a = b, P Q, trigger1{$trigger:ut2, $a:ut2, $x:ut2}(T; A; P; i; k),  A,  b,   x. t(x),  , t  T, "$x", P Q, Id, x:A. B(x), (e <loc e'), @i(x:T), Dec(P), P  Q, state after e, e' e.P(e'), (state when e), @i Precondition for a(Outcome(p)) P discrete state(ds), recognizer-p(es;T;A;P;k;i;r;x), State(ds), Unit, R ||- es.P(es),  es.P(es), False, Realizer, x(s), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(), left right, Rpre(loc;ds;a;p;P),  |
| Lemmas | Id sq, es-val wf, es-le-loc, es-locl wf, es-locl transitivity1, es-pred-locl, es-dtype wf, es-after-pred2, es-when wf, es-vartype wf, es-after wf, es-loc-pred, es-pred wf, bool sq, es-E wf, es-loc wf, es-kind wf, es-first wf, decidable assert, es-dds-single, R-sub-plus-right3, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, fpf-single wf3, unit-fps wf, discrete-pre-p wf, normal-ds wf, bool-inhabited, normal-ds-single, R-sub-plus-left, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, rationals wf, unit wf, es realizer wf, true wf, R-sub-implies, recognizer-p wf, es-real wf, false wf, assert-eq-id, eq id wf, not functionality wrt iff, bool wf, normal-type wf, lnk wf, ldst wf, Id wf, isrcv wf, assert wf, locl wf, Knd wf, not wf, R-consistent wf, event system wf, trigger1-p wf, implies-es-real, trigger1 feasible, trigger1 wf |
T
), i:Id, k:Knd.
